Left Termination proof of /tmp/tmpt8j9zk/btapplast.pl

Left Termination of the query pattern goal(b,f,f) w.r.t. the given Prolog program could successfully be proven:

↳ PROLOG

  ↳ PrologToPiTRSProof

goal₃(A, B, C) :- s2t₂(A, T), tapplast₃(T, B, C).
tapplast₃(L, X, Last) :- tappend₃(L, node₃(nil₀, X, nil₀), LX), tlast₂(Last, LX).
tlast₂(X, node₃(nil₀, X, nil₀)).
tlast₂(X, node₃(L, H, R)) :- tlast₂(X, L).
tlast₂(X, node₃(L, H, R)) :- tlast₂(X, R).
tappend₃(nil₀, T, T).
tappend₃(node₃(nil₀, X, T2), T1, node₃(T1, X, T2)).
tappend₃(node₃(T1, X, nil₀), T2, node₃(T1, X, T2)).
tappend₃(node₃(T1, X, T2), T3, node₃(U, X, T2)) :- tappend₃(T1, T3, U).
tappend₃(node₃(T1, X, T2), T3, node₃(T1, X, U)) :- tappend₃(T2, T3, U).
s2t₂(s₁(X), node₃(T, Y, T)) :- s2t₂(X, T).
s2t₂(s₁(X), node₃(nil₀, Y, T)) :- s2t₂(X, T).
s2t₂(s₁(X), node₃(T, Y, nil₀)) :- s2t₂(X, T).
s2t₂(s₁(X), node₃(nil₀, Y, nil₀)).
s2t₂(0₀, nil₀).

With regard to the inferred argument filtering the predicates were used in the following modes:
goal₃: (b,f,f)
s2t₂: (b,f)
tapplast₃: (b,f,f)
tappend₃: (b,b,f)
tlast₂: (f,b)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

goal_3_in_gaa₃(A, B, C) -> if_goal_3_in_1_gaa₄(A, B, C, s2t_2_in_ga₂(A, T))
s2t_2_in_ga₂(s_1₁(X), node_3₃(T, Y, T)) -> if_s2t_2_in_1_ga₄(X, T, Y, s2t_2_in_ga₂(X, T))
s2t_2_in_ga₂(s_1₁(X), node_3₃(nil_0, Y, T)) -> if_s2t_2_in_2_ga₄(X, Y, T, s2t_2_in_ga₂(X, T))
s2t_2_in_ga₂(s_1₁(X), node_3₃(T, Y, nil_0)) -> if_s2t_2_in_3_ga₄(X, T, Y, s2t_2_in_ga₂(X, T))
s2t_2_in_ga₂(s_1₁(X), node_3₃(nil_0, Y, nil_0)) -> s2t_2_out_ga₂(s_1₁(X), node_3₃(nil_0, Y, nil_0))
s2t_2_in_ga₂(0_0, nil_0) -> s2t_2_out_ga₂(0_0, nil_0)
if_s2t_2_in_3_ga₄(X, T, Y, s2t_2_out_ga₂(X, T)) -> s2t_2_out_ga₂(s_1₁(X), node_3₃(T, Y, nil_0))
if_s2t_2_in_2_ga₄(X, Y, T, s2t_2_out_ga₂(X, T)) -> s2t_2_out_ga₂(s_1₁(X), node_3₃(nil_0, Y, T))
if_s2t_2_in_1_ga₄(X, T, Y, s2t_2_out_ga₂(X, T)) -> s2t_2_out_ga₂(s_1₁(X), node_3₃(T, Y, T))
if_goal_3_in_1_gaa₄(A, B, C, s2t_2_out_ga₂(A, T)) -> if_goal_3_in_2_gaa₅(A, B, C, T, tapplast_3_in_gaa₃(T, B, C))
tapplast_3_in_gaa₃(L, X, Last) -> if_tapplast_3_in_1_gaa₄(L, X, Last, tappend_3_in_gga₃(L, node_3₃(nil_0, X, nil_0), LX))
tappend_3_in_gga₃(nil_0, T, T) -> tappend_3_out_gga₃(nil_0, T, T)
tappend_3_in_gga₃(node_3₃(nil_0, X, T2), T1, node_3₃(T1, X, T2)) -> tappend_3_out_gga₃(node_3₃(nil_0, X, T2), T1, node_3₃(T1, X, T2))
tappend_3_in_gga₃(node_3₃(T1, X, nil_0), T2, node_3₃(T1, X, T2)) -> tappend_3_out_gga₃(node_3₃(T1, X, nil_0), T2, node_3₃(T1, X, T2))
tappend_3_in_gga₃(node_3₃(T1, X, T2), T3, node_3₃(U, X, T2)) -> if_tappend_3_in_1_gga₆(T1, X, T2, T3, U, tappend_3_in_gga₃(T1, T3, U))
tappend_3_in_gga₃(node_3₃(T1, X, T2), T3, node_3₃(T1, X, U)) -> if_tappend_3_in_2_gga₆(T1, X, T2, T3, U, tappend_3_in_gga₃(T2, T3, U))
if_tappend_3_in_2_gga₆(T1, X, T2, T3, U, tappend_3_out_gga₃(T2, T3, U)) -> tappend_3_out_gga₃(node_3₃(T1, X, T2), T3, node_3₃(T1, X, U))
if_tappend_3_in_1_gga₆(T1, X, T2, T3, U, tappend_3_out_gga₃(T1, T3, U)) -> tappend_3_out_gga₃(node_3₃(T1, X, T2), T3, node_3₃(U, X, T2))
if_tapplast_3_in_1_gaa₄(L, X, Last, tappend_3_out_gga₃(L, node_3₃(nil_0, X, nil_0), LX)) -> if_tapplast_3_in_2_gaa₅(L, X, Last, LX, tlast_2_in_ag₂(Last, LX))
tlast_2_in_ag₂(X, node_3₃(nil_0, X, nil_0)) -> tlast_2_out_ag₂(X, node_3₃(nil_0, X, nil_0))
tlast_2_in_ag₂(X, node_3₃(L, H, R)) -> if_tlast_2_in_1_ag₅(X, L, H, R, tlast_2_in_ag₂(X, L))
tlast_2_in_ag₂(X, node_3₃(L, H, R)) -> if_tlast_2_in_2_ag₅(X, L, H, R, tlast_2_in_ag₂(X, R))
if_tlast_2_in_2_ag₅(X, L, H, R, tlast_2_out_ag₂(X, R)) -> tlast_2_out_ag₂(X, node_3₃(L, H, R))
if_tlast_2_in_1_ag₅(X, L, H, R, tlast_2_out_ag₂(X, L)) -> tlast_2_out_ag₂(X, node_3₃(L, H, R))
if_tapplast_3_in_2_gaa₅(L, X, Last, LX, tlast_2_out_ag₂(Last, LX)) -> tapplast_3_out_gaa₃(L, X, Last)
if_goal_3_in_2_gaa₅(A, B, C, T, tapplast_3_out_gaa₃(T, B, C)) -> goal_3_out_gaa₃(A, B, C)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

goal_3_in_gaa₃(A, B, C) -> if_goal_3_in_1_gaa₄(A, B, C, s2t_2_in_ga₂(A, T))
s2t_2_in_ga₂(s_1₁(X), node_3₃(T, Y, T)) -> if_s2t_2_in_1_ga₄(X, T, Y, s2t_2_in_ga₂(X, T))
s2t_2_in_ga₂(s_1₁(X), node_3₃(nil_0, Y, T)) -> if_s2t_2_in_2_ga₄(X, Y, T, s2t_2_in_ga₂(X, T))
s2t_2_in_ga₂(s_1₁(X), node_3₃(T, Y, nil_0)) -> if_s2t_2_in_3_ga₄(X, T, Y, s2t_2_in_ga₂(X, T))
s2t_2_in_ga₂(s_1₁(X), node_3₃(nil_0, Y, nil_0)) -> s2t_2_out_ga₂(s_1₁(X), node_3₃(nil_0, Y, nil_0))
s2t_2_in_ga₂(0_0, nil_0) -> s2t_2_out_ga₂(0_0, nil_0)
if_s2t_2_in_3_ga₄(X, T, Y, s2t_2_out_ga₂(X, T)) -> s2t_2_out_ga₂(s_1₁(X), node_3₃(T, Y, nil_0))
if_s2t_2_in_2_ga₄(X, Y, T, s2t_2_out_ga₂(X, T)) -> s2t_2_out_ga₂(s_1₁(X), node_3₃(nil_0, Y, T))
if_s2t_2_in_1_ga₄(X, T, Y, s2t_2_out_ga₂(X, T)) -> s2t_2_out_ga₂(s_1₁(X), node_3₃(T, Y, T))
if_goal_3_in_1_gaa₄(A, B, C, s2t_2_out_ga₂(A, T)) -> if_goal_3_in_2_gaa₅(A, B, C, T, tapplast_3_in_gaa₃(T, B, C))
tapplast_3_in_gaa₃(L, X, Last) -> if_tapplast_3_in_1_gaa₄(L, X, Last, tappend_3_in_gga₃(L, node_3₃(nil_0, X, nil_0), LX))
tappend_3_in_gga₃(nil_0, T, T) -> tappend_3_out_gga₃(nil_0, T, T)
tappend_3_in_gga₃(node_3₃(nil_0, X, T2), T1, node_3₃(T1, X, T2)) -> tappend_3_out_gga₃(node_3₃(nil_0, X, T2), T1, node_3₃(T1, X, T2))
tappend_3_in_gga₃(node_3₃(T1, X, nil_0), T2, node_3₃(T1, X, T2)) -> tappend_3_out_gga₃(node_3₃(T1, X, nil_0), T2, node_3₃(T1, X, T2))
tappend_3_in_gga₃(node_3₃(T1, X, T2), T3, node_3₃(U, X, T2)) -> if_tappend_3_in_1_gga₆(T1, X, T2, T3, U, tappend_3_in_gga₃(T1, T3, U))
tappend_3_in_gga₃(node_3₃(T1, X, T2), T3, node_3₃(T1, X, U)) -> if_tappend_3_in_2_gga₆(T1, X, T2, T3, U, tappend_3_in_gga₃(T2, T3, U))
if_tappend_3_in_2_gga₆(T1, X, T2, T3, U, tappend_3_out_gga₃(T2, T3, U)) -> tappend_3_out_gga₃(node_3₃(T1, X, T2), T3, node_3₃(T1, X, U))
if_tappend_3_in_1_gga₆(T1, X, T2, T3, U, tappend_3_out_gga₃(T1, T3, U)) -> tappend_3_out_gga₃(node_3₃(T1, X, T2), T3, node_3₃(U, X, T2))
if_tapplast_3_in_1_gaa₄(L, X, Last, tappend_3_out_gga₃(L, node_3₃(nil_0, X, nil_0), LX)) -> if_tapplast_3_in_2_gaa₅(L, X, Last, LX, tlast_2_in_ag₂(Last, LX))
tlast_2_in_ag₂(X, node_3₃(nil_0, X, nil_0)) -> tlast_2_out_ag₂(X, node_3₃(nil_0, X, nil_0))
tlast_2_in_ag₂(X, node_3₃(L, H, R)) -> if_tlast_2_in_1_ag₅(X, L, H, R, tlast_2_in_ag₂(X, L))
tlast_2_in_ag₂(X, node_3₃(L, H, R)) -> if_tlast_2_in_2_ag₅(X, L, H, R, tlast_2_in_ag₂(X, R))
if_tlast_2_in_2_ag₅(X, L, H, R, tlast_2_out_ag₂(X, R)) -> tlast_2_out_ag₂(X, node_3₃(L, H, R))
if_tlast_2_in_1_ag₅(X, L, H, R, tlast_2_out_ag₂(X, L)) -> tlast_2_out_ag₂(X, node_3₃(L, H, R))
if_tapplast_3_in_2_gaa₅(L, X, Last, LX, tlast_2_out_ag₂(Last, LX)) -> tapplast_3_out_gaa₃(L, X, Last)
if_goal_3_in_2_gaa₅(A, B, C, T, tapplast_3_out_gaa₃(T, B, C)) -> goal_3_out_gaa₃(A, B, C)

GOAL_3_IN_GAA₃(A, B, C) -> IF_GOAL_3_IN_1_GAA₄(A, B, C, s2t_2_in_ga₂(A, T))
GOAL_3_IN_GAA₃(A, B, C) -> S2T_2_IN_GA₂(A, T)
S2T_2_IN_GA₂(s_1₁(X), node_3₃(T, Y, T)) -> IF_S2T_2_IN_1_GA₄(X, T, Y, s2t_2_in_ga₂(X, T))
S2T_2_IN_GA₂(s_1₁(X), node_3₃(T, Y, T)) -> S2T_2_IN_GA₂(X, T)
S2T_2_IN_GA₂(s_1₁(X), node_3₃(nil_0, Y, T)) -> IF_S2T_2_IN_2_GA₄(X, Y, T, s2t_2_in_ga₂(X, T))
S2T_2_IN_GA₂(s_1₁(X), node_3₃(nil_0, Y, T)) -> S2T_2_IN_GA₂(X, T)
S2T_2_IN_GA₂(s_1₁(X), node_3₃(T, Y, nil_0)) -> IF_S2T_2_IN_3_GA₄(X, T, Y, s2t_2_in_ga₂(X, T))
S2T_2_IN_GA₂(s_1₁(X), node_3₃(T, Y, nil_0)) -> S2T_2_IN_GA₂(X, T)
IF_GOAL_3_IN_1_GAA₄(A, B, C, s2t_2_out_ga₂(A, T)) -> IF_GOAL_3_IN_2_GAA₅(A, B, C, T, tapplast_3_in_gaa₃(T, B, C))
IF_GOAL_3_IN_1_GAA₄(A, B, C, s2t_2_out_ga₂(A, T)) -> TAPPLAST_3_IN_GAA₃(T, B, C)
TAPPLAST_3_IN_GAA₃(L, X, Last) -> IF_TAPPLAST_3_IN_1_GAA₄(L, X, Last, tappend_3_in_gga₃(L, node_3₃(nil_0, X, nil_0), LX))
TAPPLAST_3_IN_GAA₃(L, X, Last) -> TAPPEND_3_IN_GGA₃(L, node_3₃(nil_0, X, nil_0), LX)
TAPPEND_3_IN_GGA₃(node_3₃(T1, X, T2), T3, node_3₃(U, X, T2)) -> IF_TAPPEND_3_IN_1_GGA₆(T1, X, T2, T3, U, tappend_3_in_gga₃(T1, T3, U))
TAPPEND_3_IN_GGA₃(node_3₃(T1, X, T2), T3, node_3₃(U, X, T2)) -> TAPPEND_3_IN_GGA₃(T1, T3, U)
TAPPEND_3_IN_GGA₃(node_3₃(T1, X, T2), T3, node_3₃(T1, X, U)) -> IF_TAPPEND_3_IN_2_GGA₆(T1, X, T2, T3, U, tappend_3_in_gga₃(T2, T3, U))
TAPPEND_3_IN_GGA₃(node_3₃(T1, X, T2), T3, node_3₃(T1, X, U)) -> TAPPEND_3_IN_GGA₃(T2, T3, U)
IF_TAPPLAST_3_IN_1_GAA₄(L, X, Last, tappend_3_out_gga₃(L, node_3₃(nil_0, X, nil_0), LX)) -> IF_TAPPLAST_3_IN_2_GAA₅(L, X, Last, LX, tlast_2_in_ag₂(Last, LX))
IF_TAPPLAST_3_IN_1_GAA₄(L, X, Last, tappend_3_out_gga₃(L, node_3₃(nil_0, X, nil_0), LX)) -> TLAST_2_IN_AG₂(Last, LX)
TLAST_2_IN_AG₂(X, node_3₃(L, H, R)) -> IF_TLAST_2_IN_1_AG₅(X, L, H, R, tlast_2_in_ag₂(X, L))
TLAST_2_IN_AG₂(X, node_3₃(L, H, R)) -> TLAST_2_IN_AG₂(X, L)
TLAST_2_IN_AG₂(X, node_3₃(L, H, R)) -> IF_TLAST_2_IN_2_AG₅(X, L, H, R, tlast_2_in_ag₂(X, R))
TLAST_2_IN_AG₂(X, node_3₃(L, H, R)) -> TLAST_2_IN_AG₂(X, R)

The TRS R consists of the following rules:

goal_3_in_gaa₃(A, B, C) -> if_goal_3_in_1_gaa₄(A, B, C, s2t_2_in_ga₂(A, T))
s2t_2_in_ga₂(s_1₁(X), node_3₃(T, Y, T)) -> if_s2t_2_in_1_ga₄(X, T, Y, s2t_2_in_ga₂(X, T))
s2t_2_in_ga₂(s_1₁(X), node_3₃(nil_0, Y, T)) -> if_s2t_2_in_2_ga₄(X, Y, T, s2t_2_in_ga₂(X, T))
s2t_2_in_ga₂(s_1₁(X), node_3₃(T, Y, nil_0)) -> if_s2t_2_in_3_ga₄(X, T, Y, s2t_2_in_ga₂(X, T))
s2t_2_in_ga₂(s_1₁(X), node_3₃(nil_0, Y, nil_0)) -> s2t_2_out_ga₂(s_1₁(X), node_3₃(nil_0, Y, nil_0))
s2t_2_in_ga₂(0_0, nil_0) -> s2t_2_out_ga₂(0_0, nil_0)
if_s2t_2_in_3_ga₄(X, T, Y, s2t_2_out_ga₂(X, T)) -> s2t_2_out_ga₂(s_1₁(X), node_3₃(T, Y, nil_0))
if_s2t_2_in_2_ga₄(X, Y, T, s2t_2_out_ga₂(X, T)) -> s2t_2_out_ga₂(s_1₁(X), node_3₃(nil_0, Y, T))
if_s2t_2_in_1_ga₄(X, T, Y, s2t_2_out_ga₂(X, T)) -> s2t_2_out_ga₂(s_1₁(X), node_3₃(T, Y, T))
if_goal_3_in_1_gaa₄(A, B, C, s2t_2_out_ga₂(A, T)) -> if_goal_3_in_2_gaa₅(A, B, C, T, tapplast_3_in_gaa₃(T, B, C))
tapplast_3_in_gaa₃(L, X, Last) -> if_tapplast_3_in_1_gaa₄(L, X, Last, tappend_3_in_gga₃(L, node_3₃(nil_0, X, nil_0), LX))
tappend_3_in_gga₃(nil_0, T, T) -> tappend_3_out_gga₃(nil_0, T, T)
tappend_3_in_gga₃(node_3₃(nil_0, X, T2), T1, node_3₃(T1, X, T2)) -> tappend_3_out_gga₃(node_3₃(nil_0, X, T2), T1, node_3₃(T1, X, T2))
tappend_3_in_gga₃(node_3₃(T1, X, nil_0), T2, node_3₃(T1, X, T2)) -> tappend_3_out_gga₃(node_3₃(T1, X, nil_0), T2, node_3₃(T1, X, T2))
tappend_3_in_gga₃(node_3₃(T1, X, T2), T3, node_3₃(U, X, T2)) -> if_tappend_3_in_1_gga₆(T1, X, T2, T3, U, tappend_3_in_gga₃(T1, T3, U))
tappend_3_in_gga₃(node_3₃(T1, X, T2), T3, node_3₃(T1, X, U)) -> if_tappend_3_in_2_gga₆(T1, X, T2, T3, U, tappend_3_in_gga₃(T2, T3, U))
if_tappend_3_in_2_gga₆(T1, X, T2, T3, U, tappend_3_out_gga₃(T2, T3, U)) -> tappend_3_out_gga₃(node_3₃(T1, X, T2), T3, node_3₃(T1, X, U))
if_tappend_3_in_1_gga₆(T1, X, T2, T3, U, tappend_3_out_gga₃(T1, T3, U)) -> tappend_3_out_gga₃(node_3₃(T1, X, T2), T3, node_3₃(U, X, T2))
if_tapplast_3_in_1_gaa₄(L, X, Last, tappend_3_out_gga₃(L, node_3₃(nil_0, X, nil_0), LX)) -> if_tapplast_3_in_2_gaa₅(L, X, Last, LX, tlast_2_in_ag₂(Last, LX))
tlast_2_in_ag₂(X, node_3₃(nil_0, X, nil_0)) -> tlast_2_out_ag₂(X, node_3₃(nil_0, X, nil_0))
tlast_2_in_ag₂(X, node_3₃(L, H, R)) -> if_tlast_2_in_1_ag₅(X, L, H, R, tlast_2_in_ag₂(X, L))
tlast_2_in_ag₂(X, node_3₃(L, H, R)) -> if_tlast_2_in_2_ag₅(X, L, H, R, tlast_2_in_ag₂(X, R))
if_tlast_2_in_2_ag₅(X, L, H, R, tlast_2_out_ag₂(X, R)) -> tlast_2_out_ag₂(X, node_3₃(L, H, R))
if_tlast_2_in_1_ag₅(X, L, H, R, tlast_2_out_ag₂(X, L)) -> tlast_2_out_ag₂(X, node_3₃(L, H, R))
if_tapplast_3_in_2_gaa₅(L, X, Last, LX, tlast_2_out_ag₂(Last, LX)) -> tapplast_3_out_gaa₃(L, X, Last)
if_goal_3_in_2_gaa₅(A, B, C, T, tapplast_3_out_gaa₃(T, B, C)) -> goal_3_out_gaa₃(A, B, C)

The argument filtering Pi contains the following mapping:
goal_3_in_gaa₃(x1, x2, x3) = goal_3_in_gaa₁(x1)
node_3₃(x1, x2, x3) = node_3₂(x1, x3)
nil_0 = nil_0
s_1₁(x1) = s_1₁(x1)
0_0 = 0_0
if_goal_3_in_1_gaa₄(x1, x2, x3, x4) = if_goal_3_in_1_gaa₁(x4)
s2t_2_in_ga₂(x1, x2) = s2t_2_in_ga₁(x1)
if_s2t_2_in_1_ga₄(x1, x2, x3, x4) = if_s2t_2_in_1_ga₁(x4)
if_s2t_2_in_2_ga₄(x1, x2, x3, x4) = if_s2t_2_in_2_ga₁(x4)
if_s2t_2_in_3_ga₄(x1, x2, x3, x4) = if_s2t_2_in_3_ga₁(x4)
s2t_2_out_ga₂(x1, x2) = s2t_2_out_ga₁(x2)
if_goal_3_in_2_gaa₅(x1, x2, x3, x4, x5) = if_goal_3_in_2_gaa₁(x5)
tapplast_3_in_gaa₃(x1, x2, x3) = tapplast_3_in_gaa₁(x1)
if_tapplast_3_in_1_gaa₄(x1, x2, x3, x4) = if_tapplast_3_in_1_gaa₁(x4)
tappend_3_in_gga₃(x1, x2, x3) = tappend_3_in_gga₂(x1, x2)
tappend_3_out_gga₃(x1, x2, x3) = tappend_3_out_gga₁(x3)
if_tappend_3_in_1_gga₆(x1, x2, x3, x4, x5, x6) = if_tappend_3_in_1_gga₂(x3, x6)
if_tappend_3_in_2_gga₆(x1, x2, x3, x4, x5, x6) = if_tappend_3_in_2_gga₂(x1, x6)
if_tapplast_3_in_2_gaa₅(x1, x2, x3, x4, x5) = if_tapplast_3_in_2_gaa₁(x5)
tlast_2_in_ag₂(x1, x2) = tlast_2_in_ag₁(x2)
tlast_2_out_ag₂(x1, x2) = tlast_2_out_ag
if_tlast_2_in_1_ag₅(x1, x2, x3, x4, x5) = if_tlast_2_in_1_ag₁(x5)
if_tlast_2_in_2_ag₅(x1, x2, x3, x4, x5) = if_tlast_2_in_2_ag₁(x5)
tapplast_3_out_gaa₃(x1, x2, x3) = tapplast_3_out_gaa
goal_3_out_gaa₃(x1, x2, x3) = goal_3_out_gaa
S2T_2_IN_GA₂(x1, x2) = S2T_2_IN_GA₁(x1)
IF_S2T_2_IN_3_GA₄(x1, x2, x3, x4) = IF_S2T_2_IN_3_GA₁(x4)
IF_TLAST_2_IN_1_AG₅(x1, x2, x3, x4, x5) = IF_TLAST_2_IN_1_AG₁(x5)
GOAL_3_IN_GAA₃(x1, x2, x3) = GOAL_3_IN_GAA₁(x1)
IF_GOAL_3_IN_2_GAA₅(x1, x2, x3, x4, x5) = IF_GOAL_3_IN_2_GAA₁(x5)
TAPPLAST_3_IN_GAA₃(x1, x2, x3) = TAPPLAST_3_IN_GAA₁(x1)
IF_S2T_2_IN_1_GA₄(x1, x2, x3, x4) = IF_S2T_2_IN_1_GA₁(x4)
IF_TAPPEND_3_IN_1_GGA₆(x1, x2, x3, x4, x5, x6) = IF_TAPPEND_3_IN_1_GGA₂(x3, x6)
IF_GOAL_3_IN_1_GAA₄(x1, x2, x3, x4) = IF_GOAL_3_IN_1_GAA₁(x4)
TAPPEND_3_IN_GGA₃(x1, x2, x3) = TAPPEND_3_IN_GGA₂(x1, x2)
IF_TAPPLAST_3_IN_1_GAA₄(x1, x2, x3, x4) = IF_TAPPLAST_3_IN_1_GAA₁(x4)
IF_TAPPEND_3_IN_2_GGA₆(x1, x2, x3, x4, x5, x6) = IF_TAPPEND_3_IN_2_GGA₂(x1, x6)
IF_TAPPLAST_3_IN_2_GAA₅(x1, x2, x3, x4, x5) = IF_TAPPLAST_3_IN_2_GAA₁(x5)
IF_TLAST_2_IN_2_AG₅(x1, x2, x3, x4, x5) = IF_TLAST_2_IN_2_AG₁(x5)
TLAST_2_IN_AG₂(x1, x2) = TLAST_2_IN_AG₁(x2)
IF_S2T_2_IN_2_GA₄(x1, x2, x3, x4) = IF_S2T_2_IN_2_GA₁(x4)

We have to consider all (P,R,Pi)-chains

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

GOAL_3_IN_GAA₃(A, B, C) -> IF_GOAL_3_IN_1_GAA₄(A, B, C, s2t_2_in_ga₂(A, T))
GOAL_3_IN_GAA₃(A, B, C) -> S2T_2_IN_GA₂(A, T)
S2T_2_IN_GA₂(s_1₁(X), node_3₃(T, Y, T)) -> IF_S2T_2_IN_1_GA₄(X, T, Y, s2t_2_in_ga₂(X, T))
S2T_2_IN_GA₂(s_1₁(X), node_3₃(T, Y, T)) -> S2T_2_IN_GA₂(X, T)
S2T_2_IN_GA₂(s_1₁(X), node_3₃(nil_0, Y, T)) -> IF_S2T_2_IN_2_GA₄(X, Y, T, s2t_2_in_ga₂(X, T))
S2T_2_IN_GA₂(s_1₁(X), node_3₃(nil_0, Y, T)) -> S2T_2_IN_GA₂(X, T)
S2T_2_IN_GA₂(s_1₁(X), node_3₃(T, Y, nil_0)) -> IF_S2T_2_IN_3_GA₄(X, T, Y, s2t_2_in_ga₂(X, T))
S2T_2_IN_GA₂(s_1₁(X), node_3₃(T, Y, nil_0)) -> S2T_2_IN_GA₂(X, T)
IF_GOAL_3_IN_1_GAA₄(A, B, C, s2t_2_out_ga₂(A, T)) -> IF_GOAL_3_IN_2_GAA₅(A, B, C, T, tapplast_3_in_gaa₃(T, B, C))
IF_GOAL_3_IN_1_GAA₄(A, B, C, s2t_2_out_ga₂(A, T)) -> TAPPLAST_3_IN_GAA₃(T, B, C)
TAPPLAST_3_IN_GAA₃(L, X, Last) -> IF_TAPPLAST_3_IN_1_GAA₄(L, X, Last, tappend_3_in_gga₃(L, node_3₃(nil_0, X, nil_0), LX))
TAPPLAST_3_IN_GAA₃(L, X, Last) -> TAPPEND_3_IN_GGA₃(L, node_3₃(nil_0, X, nil_0), LX)
TAPPEND_3_IN_GGA₃(node_3₃(T1, X, T2), T3, node_3₃(U, X, T2)) -> IF_TAPPEND_3_IN_1_GGA₆(T1, X, T2, T3, U, tappend_3_in_gga₃(T1, T3, U))
TAPPEND_3_IN_GGA₃(node_3₃(T1, X, T2), T3, node_3₃(U, X, T2)) -> TAPPEND_3_IN_GGA₃(T1, T3, U)
TAPPEND_3_IN_GGA₃(node_3₃(T1, X, T2), T3, node_3₃(T1, X, U)) -> IF_TAPPEND_3_IN_2_GGA₆(T1, X, T2, T3, U, tappend_3_in_gga₃(T2, T3, U))
TAPPEND_3_IN_GGA₃(node_3₃(T1, X, T2), T3, node_3₃(T1, X, U)) -> TAPPEND_3_IN_GGA₃(T2, T3, U)
IF_TAPPLAST_3_IN_1_GAA₄(L, X, Last, tappend_3_out_gga₃(L, node_3₃(nil_0, X, nil_0), LX)) -> IF_TAPPLAST_3_IN_2_GAA₅(L, X, Last, LX, tlast_2_in_ag₂(Last, LX))
IF_TAPPLAST_3_IN_1_GAA₄(L, X, Last, tappend_3_out_gga₃(L, node_3₃(nil_0, X, nil_0), LX)) -> TLAST_2_IN_AG₂(Last, LX)
TLAST_2_IN_AG₂(X, node_3₃(L, H, R)) -> IF_TLAST_2_IN_1_AG₅(X, L, H, R, tlast_2_in_ag₂(X, L))
TLAST_2_IN_AG₂(X, node_3₃(L, H, R)) -> TLAST_2_IN_AG₂(X, L)
TLAST_2_IN_AG₂(X, node_3₃(L, H, R)) -> IF_TLAST_2_IN_2_AG₅(X, L, H, R, tlast_2_in_ag₂(X, R))
TLAST_2_IN_AG₂(X, node_3₃(L, H, R)) -> TLAST_2_IN_AG₂(X, R)

The TRS R consists of the following rules:

goal_3_in_gaa₃(A, B, C) -> if_goal_3_in_1_gaa₄(A, B, C, s2t_2_in_ga₂(A, T))
s2t_2_in_ga₂(s_1₁(X), node_3₃(T, Y, T)) -> if_s2t_2_in_1_ga₄(X, T, Y, s2t_2_in_ga₂(X, T))
s2t_2_in_ga₂(s_1₁(X), node_3₃(nil_0, Y, T)) -> if_s2t_2_in_2_ga₄(X, Y, T, s2t_2_in_ga₂(X, T))
s2t_2_in_ga₂(s_1₁(X), node_3₃(T, Y, nil_0)) -> if_s2t_2_in_3_ga₄(X, T, Y, s2t_2_in_ga₂(X, T))
s2t_2_in_ga₂(s_1₁(X), node_3₃(nil_0, Y, nil_0)) -> s2t_2_out_ga₂(s_1₁(X), node_3₃(nil_0, Y, nil_0))
s2t_2_in_ga₂(0_0, nil_0) -> s2t_2_out_ga₂(0_0, nil_0)
if_s2t_2_in_3_ga₄(X, T, Y, s2t_2_out_ga₂(X, T)) -> s2t_2_out_ga₂(s_1₁(X), node_3₃(T, Y, nil_0))
if_s2t_2_in_2_ga₄(X, Y, T, s2t_2_out_ga₂(X, T)) -> s2t_2_out_ga₂(s_1₁(X), node_3₃(nil_0, Y, T))
if_s2t_2_in_1_ga₄(X, T, Y, s2t_2_out_ga₂(X, T)) -> s2t_2_out_ga₂(s_1₁(X), node_3₃(T, Y, T))
if_goal_3_in_1_gaa₄(A, B, C, s2t_2_out_ga₂(A, T)) -> if_goal_3_in_2_gaa₅(A, B, C, T, tapplast_3_in_gaa₃(T, B, C))
tapplast_3_in_gaa₃(L, X, Last) -> if_tapplast_3_in_1_gaa₄(L, X, Last, tappend_3_in_gga₃(L, node_3₃(nil_0, X, nil_0), LX))
tappend_3_in_gga₃(nil_0, T, T) -> tappend_3_out_gga₃(nil_0, T, T)
tappend_3_in_gga₃(node_3₃(nil_0, X, T2), T1, node_3₃(T1, X, T2)) -> tappend_3_out_gga₃(node_3₃(nil_0, X, T2), T1, node_3₃(T1, X, T2))
tappend_3_in_gga₃(node_3₃(T1, X, nil_0), T2, node_3₃(T1, X, T2)) -> tappend_3_out_gga₃(node_3₃(T1, X, nil_0), T2, node_3₃(T1, X, T2))
tappend_3_in_gga₃(node_3₃(T1, X, T2), T3, node_3₃(U, X, T2)) -> if_tappend_3_in_1_gga₆(T1, X, T2, T3, U, tappend_3_in_gga₃(T1, T3, U))
tappend_3_in_gga₃(node_3₃(T1, X, T2), T3, node_3₃(T1, X, U)) -> if_tappend_3_in_2_gga₆(T1, X, T2, T3, U, tappend_3_in_gga₃(T2, T3, U))
if_tappend_3_in_2_gga₆(T1, X, T2, T3, U, tappend_3_out_gga₃(T2, T3, U)) -> tappend_3_out_gga₃(node_3₃(T1, X, T2), T3, node_3₃(T1, X, U))
if_tappend_3_in_1_gga₆(T1, X, T2, T3, U, tappend_3_out_gga₃(T1, T3, U)) -> tappend_3_out_gga₃(node_3₃(T1, X, T2), T3, node_3₃(U, X, T2))
if_tapplast_3_in_1_gaa₄(L, X, Last, tappend_3_out_gga₃(L, node_3₃(nil_0, X, nil_0), LX)) -> if_tapplast_3_in_2_gaa₅(L, X, Last, LX, tlast_2_in_ag₂(Last, LX))
tlast_2_in_ag₂(X, node_3₃(nil_0, X, nil_0)) -> tlast_2_out_ag₂(X, node_3₃(nil_0, X, nil_0))
tlast_2_in_ag₂(X, node_3₃(L, H, R)) -> if_tlast_2_in_1_ag₅(X, L, H, R, tlast_2_in_ag₂(X, L))
tlast_2_in_ag₂(X, node_3₃(L, H, R)) -> if_tlast_2_in_2_ag₅(X, L, H, R, tlast_2_in_ag₂(X, R))
if_tlast_2_in_2_ag₅(X, L, H, R, tlast_2_out_ag₂(X, R)) -> tlast_2_out_ag₂(X, node_3₃(L, H, R))
if_tlast_2_in_1_ag₅(X, L, H, R, tlast_2_out_ag₂(X, L)) -> tlast_2_out_ag₂(X, node_3₃(L, H, R))
if_tapplast_3_in_2_gaa₅(L, X, Last, LX, tlast_2_out_ag₂(Last, LX)) -> tapplast_3_out_gaa₃(L, X, Last)
if_goal_3_in_2_gaa₅(A, B, C, T, tapplast_3_out_gaa₃(T, B, C)) -> goal_3_out_gaa₃(A, B, C)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

TLAST_2_IN_AG₂(X, node_3₃(L, H, R)) -> TLAST_2_IN_AG₂(X, R)
TLAST_2_IN_AG₂(X, node_3₃(L, H, R)) -> TLAST_2_IN_AG₂(X, L)

The TRS R consists of the following rules:

goal_3_in_gaa₃(A, B, C) -> if_goal_3_in_1_gaa₄(A, B, C, s2t_2_in_ga₂(A, T))
s2t_2_in_ga₂(s_1₁(X), node_3₃(T, Y, T)) -> if_s2t_2_in_1_ga₄(X, T, Y, s2t_2_in_ga₂(X, T))
s2t_2_in_ga₂(s_1₁(X), node_3₃(nil_0, Y, T)) -> if_s2t_2_in_2_ga₄(X, Y, T, s2t_2_in_ga₂(X, T))
s2t_2_in_ga₂(s_1₁(X), node_3₃(T, Y, nil_0)) -> if_s2t_2_in_3_ga₄(X, T, Y, s2t_2_in_ga₂(X, T))
s2t_2_in_ga₂(s_1₁(X), node_3₃(nil_0, Y, nil_0)) -> s2t_2_out_ga₂(s_1₁(X), node_3₃(nil_0, Y, nil_0))
s2t_2_in_ga₂(0_0, nil_0) -> s2t_2_out_ga₂(0_0, nil_0)
if_s2t_2_in_3_ga₄(X, T, Y, s2t_2_out_ga₂(X, T)) -> s2t_2_out_ga₂(s_1₁(X), node_3₃(T, Y, nil_0))
if_s2t_2_in_2_ga₄(X, Y, T, s2t_2_out_ga₂(X, T)) -> s2t_2_out_ga₂(s_1₁(X), node_3₃(nil_0, Y, T))
if_s2t_2_in_1_ga₄(X, T, Y, s2t_2_out_ga₂(X, T)) -> s2t_2_out_ga₂(s_1₁(X), node_3₃(T, Y, T))
if_goal_3_in_1_gaa₄(A, B, C, s2t_2_out_ga₂(A, T)) -> if_goal_3_in_2_gaa₅(A, B, C, T, tapplast_3_in_gaa₃(T, B, C))
tapplast_3_in_gaa₃(L, X, Last) -> if_tapplast_3_in_1_gaa₄(L, X, Last, tappend_3_in_gga₃(L, node_3₃(nil_0, X, nil_0), LX))
tappend_3_in_gga₃(nil_0, T, T) -> tappend_3_out_gga₃(nil_0, T, T)
tappend_3_in_gga₃(node_3₃(nil_0, X, T2), T1, node_3₃(T1, X, T2)) -> tappend_3_out_gga₃(node_3₃(nil_0, X, T2), T1, node_3₃(T1, X, T2))
tappend_3_in_gga₃(node_3₃(T1, X, nil_0), T2, node_3₃(T1, X, T2)) -> tappend_3_out_gga₃(node_3₃(T1, X, nil_0), T2, node_3₃(T1, X, T2))
tappend_3_in_gga₃(node_3₃(T1, X, T2), T3, node_3₃(U, X, T2)) -> if_tappend_3_in_1_gga₆(T1, X, T2, T3, U, tappend_3_in_gga₃(T1, T3, U))
tappend_3_in_gga₃(node_3₃(T1, X, T2), T3, node_3₃(T1, X, U)) -> if_tappend_3_in_2_gga₆(T1, X, T2, T3, U, tappend_3_in_gga₃(T2, T3, U))
if_tappend_3_in_2_gga₆(T1, X, T2, T3, U, tappend_3_out_gga₃(T2, T3, U)) -> tappend_3_out_gga₃(node_3₃(T1, X, T2), T3, node_3₃(T1, X, U))
if_tappend_3_in_1_gga₆(T1, X, T2, T3, U, tappend_3_out_gga₃(T1, T3, U)) -> tappend_3_out_gga₃(node_3₃(T1, X, T2), T3, node_3₃(U, X, T2))
if_tapplast_3_in_1_gaa₄(L, X, Last, tappend_3_out_gga₃(L, node_3₃(nil_0, X, nil_0), LX)) -> if_tapplast_3_in_2_gaa₅(L, X, Last, LX, tlast_2_in_ag₂(Last, LX))
tlast_2_in_ag₂(X, node_3₃(nil_0, X, nil_0)) -> tlast_2_out_ag₂(X, node_3₃(nil_0, X, nil_0))
tlast_2_in_ag₂(X, node_3₃(L, H, R)) -> if_tlast_2_in_1_ag₅(X, L, H, R, tlast_2_in_ag₂(X, L))
tlast_2_in_ag₂(X, node_3₃(L, H, R)) -> if_tlast_2_in_2_ag₅(X, L, H, R, tlast_2_in_ag₂(X, R))
if_tlast_2_in_2_ag₅(X, L, H, R, tlast_2_out_ag₂(X, R)) -> tlast_2_out_ag₂(X, node_3₃(L, H, R))
if_tlast_2_in_1_ag₅(X, L, H, R, tlast_2_out_ag₂(X, L)) -> tlast_2_out_ag₂(X, node_3₃(L, H, R))
if_tapplast_3_in_2_gaa₅(L, X, Last, LX, tlast_2_out_ag₂(Last, LX)) -> tapplast_3_out_gaa₃(L, X, Last)
if_goal_3_in_2_gaa₅(A, B, C, T, tapplast_3_out_gaa₃(T, B, C)) -> goal_3_out_gaa₃(A, B, C)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

TLAST_2_IN_AG₂(X, node_3₃(L, H, R)) -> TLAST_2_IN_AG₂(X, R)
TLAST_2_IN_AG₂(X, node_3₃(L, H, R)) -> TLAST_2_IN_AG₂(X, L)

R is empty.
The argument filtering Pi contains the following mapping:
node_3₃(x1, x2, x3) = node_3₂(x1, x3)
TLAST_2_IN_AG₂(x1, x2) = TLAST_2_IN_AG₁(x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

TLAST_2_IN_AG₁(node_3₂(L, R)) -> TLAST_2_IN_AG₁(R)
TLAST_2_IN_AG₁(node_3₂(L, R)) -> TLAST_2_IN_AG₁(L)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {TLAST_2_IN_AG₁}.
By using the subterm criterion together with the size-change analysis we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

TLAST_2_IN_AG₁(node_3₂(L, R)) -> TLAST_2_IN_AG₁(R)
The graph contains the following edges 1 > 1
TLAST_2_IN_AG₁(node_3₂(L, R)) -> TLAST_2_IN_AG₁(L)
The graph contains the following edges 1 > 1

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

TAPPEND_3_IN_GGA₃(node_3₃(T1, X, T2), T3, node_3₃(T1, X, U)) -> TAPPEND_3_IN_GGA₃(T2, T3, U)
TAPPEND_3_IN_GGA₃(node_3₃(T1, X, T2), T3, node_3₃(U, X, T2)) -> TAPPEND_3_IN_GGA₃(T1, T3, U)

The TRS R consists of the following rules:

goal_3_in_gaa₃(A, B, C) -> if_goal_3_in_1_gaa₄(A, B, C, s2t_2_in_ga₂(A, T))
s2t_2_in_ga₂(s_1₁(X), node_3₃(T, Y, T)) -> if_s2t_2_in_1_ga₄(X, T, Y, s2t_2_in_ga₂(X, T))
s2t_2_in_ga₂(s_1₁(X), node_3₃(nil_0, Y, T)) -> if_s2t_2_in_2_ga₄(X, Y, T, s2t_2_in_ga₂(X, T))
s2t_2_in_ga₂(s_1₁(X), node_3₃(T, Y, nil_0)) -> if_s2t_2_in_3_ga₄(X, T, Y, s2t_2_in_ga₂(X, T))
s2t_2_in_ga₂(s_1₁(X), node_3₃(nil_0, Y, nil_0)) -> s2t_2_out_ga₂(s_1₁(X), node_3₃(nil_0, Y, nil_0))
s2t_2_in_ga₂(0_0, nil_0) -> s2t_2_out_ga₂(0_0, nil_0)
if_s2t_2_in_3_ga₄(X, T, Y, s2t_2_out_ga₂(X, T)) -> s2t_2_out_ga₂(s_1₁(X), node_3₃(T, Y, nil_0))
if_s2t_2_in_2_ga₄(X, Y, T, s2t_2_out_ga₂(X, T)) -> s2t_2_out_ga₂(s_1₁(X), node_3₃(nil_0, Y, T))
if_s2t_2_in_1_ga₄(X, T, Y, s2t_2_out_ga₂(X, T)) -> s2t_2_out_ga₂(s_1₁(X), node_3₃(T, Y, T))
if_goal_3_in_1_gaa₄(A, B, C, s2t_2_out_ga₂(A, T)) -> if_goal_3_in_2_gaa₅(A, B, C, T, tapplast_3_in_gaa₃(T, B, C))
tapplast_3_in_gaa₃(L, X, Last) -> if_tapplast_3_in_1_gaa₄(L, X, Last, tappend_3_in_gga₃(L, node_3₃(nil_0, X, nil_0), LX))
tappend_3_in_gga₃(nil_0, T, T) -> tappend_3_out_gga₃(nil_0, T, T)
tappend_3_in_gga₃(node_3₃(nil_0, X, T2), T1, node_3₃(T1, X, T2)) -> tappend_3_out_gga₃(node_3₃(nil_0, X, T2), T1, node_3₃(T1, X, T2))
tappend_3_in_gga₃(node_3₃(T1, X, nil_0), T2, node_3₃(T1, X, T2)) -> tappend_3_out_gga₃(node_3₃(T1, X, nil_0), T2, node_3₃(T1, X, T2))
tappend_3_in_gga₃(node_3₃(T1, X, T2), T3, node_3₃(U, X, T2)) -> if_tappend_3_in_1_gga₆(T1, X, T2, T3, U, tappend_3_in_gga₃(T1, T3, U))
tappend_3_in_gga₃(node_3₃(T1, X, T2), T3, node_3₃(T1, X, U)) -> if_tappend_3_in_2_gga₆(T1, X, T2, T3, U, tappend_3_in_gga₃(T2, T3, U))
if_tappend_3_in_2_gga₆(T1, X, T2, T3, U, tappend_3_out_gga₃(T2, T3, U)) -> tappend_3_out_gga₃(node_3₃(T1, X, T2), T3, node_3₃(T1, X, U))
if_tappend_3_in_1_gga₆(T1, X, T2, T3, U, tappend_3_out_gga₃(T1, T3, U)) -> tappend_3_out_gga₃(node_3₃(T1, X, T2), T3, node_3₃(U, X, T2))
if_tapplast_3_in_1_gaa₄(L, X, Last, tappend_3_out_gga₃(L, node_3₃(nil_0, X, nil_0), LX)) -> if_tapplast_3_in_2_gaa₅(L, X, Last, LX, tlast_2_in_ag₂(Last, LX))
tlast_2_in_ag₂(X, node_3₃(nil_0, X, nil_0)) -> tlast_2_out_ag₂(X, node_3₃(nil_0, X, nil_0))
tlast_2_in_ag₂(X, node_3₃(L, H, R)) -> if_tlast_2_in_1_ag₅(X, L, H, R, tlast_2_in_ag₂(X, L))
tlast_2_in_ag₂(X, node_3₃(L, H, R)) -> if_tlast_2_in_2_ag₅(X, L, H, R, tlast_2_in_ag₂(X, R))
if_tlast_2_in_2_ag₅(X, L, H, R, tlast_2_out_ag₂(X, R)) -> tlast_2_out_ag₂(X, node_3₃(L, H, R))
if_tlast_2_in_1_ag₅(X, L, H, R, tlast_2_out_ag₂(X, L)) -> tlast_2_out_ag₂(X, node_3₃(L, H, R))
if_tapplast_3_in_2_gaa₅(L, X, Last, LX, tlast_2_out_ag₂(Last, LX)) -> tapplast_3_out_gaa₃(L, X, Last)
if_goal_3_in_2_gaa₅(A, B, C, T, tapplast_3_out_gaa₃(T, B, C)) -> goal_3_out_gaa₃(A, B, C)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

TAPPEND_3_IN_GGA₃(node_3₃(T1, X, T2), T3, node_3₃(T1, X, U)) -> TAPPEND_3_IN_GGA₃(T2, T3, U)
TAPPEND_3_IN_GGA₃(node_3₃(T1, X, T2), T3, node_3₃(U, X, T2)) -> TAPPEND_3_IN_GGA₃(T1, T3, U)

R is empty.
The argument filtering Pi contains the following mapping:
node_3₃(x1, x2, x3) = node_3₂(x1, x3)
TAPPEND_3_IN_GGA₃(x1, x2, x3) = TAPPEND_3_IN_GGA₂(x1, x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

TAPPEND_3_IN_GGA₂(node_3₂(T1, T2), T3) -> TAPPEND_3_IN_GGA₂(T2, T3)
TAPPEND_3_IN_GGA₂(node_3₂(T1, T2), T3) -> TAPPEND_3_IN_GGA₂(T1, T3)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {TAPPEND_3_IN_GGA₂}.
By using the subterm criterion together with the size-change analysis we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

TAPPEND_3_IN_GGA₂(node_3₂(T1, T2), T3) -> TAPPEND_3_IN_GGA₂(T2, T3)
The graph contains the following edges 1 > 1, 2 >= 2
TAPPEND_3_IN_GGA₂(node_3₂(T1, T2), T3) -> TAPPEND_3_IN_GGA₂(T1, T3)
The graph contains the following edges 1 > 1, 2 >= 2

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

Pi DP problem:
The TRS P consists of the following rules:

S2T_2_IN_GA₂(s_1₁(X), node_3₃(T, Y, nil_0)) -> S2T_2_IN_GA₂(X, T)
S2T_2_IN_GA₂(s_1₁(X), node_3₃(nil_0, Y, T)) -> S2T_2_IN_GA₂(X, T)
S2T_2_IN_GA₂(s_1₁(X), node_3₃(T, Y, T)) -> S2T_2_IN_GA₂(X, T)

The TRS R consists of the following rules:

goal_3_in_gaa₃(A, B, C) -> if_goal_3_in_1_gaa₄(A, B, C, s2t_2_in_ga₂(A, T))
s2t_2_in_ga₂(s_1₁(X), node_3₃(T, Y, T)) -> if_s2t_2_in_1_ga₄(X, T, Y, s2t_2_in_ga₂(X, T))
s2t_2_in_ga₂(s_1₁(X), node_3₃(nil_0, Y, T)) -> if_s2t_2_in_2_ga₄(X, Y, T, s2t_2_in_ga₂(X, T))
s2t_2_in_ga₂(s_1₁(X), node_3₃(T, Y, nil_0)) -> if_s2t_2_in_3_ga₄(X, T, Y, s2t_2_in_ga₂(X, T))
s2t_2_in_ga₂(s_1₁(X), node_3₃(nil_0, Y, nil_0)) -> s2t_2_out_ga₂(s_1₁(X), node_3₃(nil_0, Y, nil_0))
s2t_2_in_ga₂(0_0, nil_0) -> s2t_2_out_ga₂(0_0, nil_0)
if_s2t_2_in_3_ga₄(X, T, Y, s2t_2_out_ga₂(X, T)) -> s2t_2_out_ga₂(s_1₁(X), node_3₃(T, Y, nil_0))
if_s2t_2_in_2_ga₄(X, Y, T, s2t_2_out_ga₂(X, T)) -> s2t_2_out_ga₂(s_1₁(X), node_3₃(nil_0, Y, T))
if_s2t_2_in_1_ga₄(X, T, Y, s2t_2_out_ga₂(X, T)) -> s2t_2_out_ga₂(s_1₁(X), node_3₃(T, Y, T))
if_goal_3_in_1_gaa₄(A, B, C, s2t_2_out_ga₂(A, T)) -> if_goal_3_in_2_gaa₅(A, B, C, T, tapplast_3_in_gaa₃(T, B, C))
tapplast_3_in_gaa₃(L, X, Last) -> if_tapplast_3_in_1_gaa₄(L, X, Last, tappend_3_in_gga₃(L, node_3₃(nil_0, X, nil_0), LX))
tappend_3_in_gga₃(nil_0, T, T) -> tappend_3_out_gga₃(nil_0, T, T)
tappend_3_in_gga₃(node_3₃(nil_0, X, T2), T1, node_3₃(T1, X, T2)) -> tappend_3_out_gga₃(node_3₃(nil_0, X, T2), T1, node_3₃(T1, X, T2))
tappend_3_in_gga₃(node_3₃(T1, X, nil_0), T2, node_3₃(T1, X, T2)) -> tappend_3_out_gga₃(node_3₃(T1, X, nil_0), T2, node_3₃(T1, X, T2))
tappend_3_in_gga₃(node_3₃(T1, X, T2), T3, node_3₃(U, X, T2)) -> if_tappend_3_in_1_gga₆(T1, X, T2, T3, U, tappend_3_in_gga₃(T1, T3, U))
tappend_3_in_gga₃(node_3₃(T1, X, T2), T3, node_3₃(T1, X, U)) -> if_tappend_3_in_2_gga₆(T1, X, T2, T3, U, tappend_3_in_gga₃(T2, T3, U))
if_tappend_3_in_2_gga₆(T1, X, T2, T3, U, tappend_3_out_gga₃(T2, T3, U)) -> tappend_3_out_gga₃(node_3₃(T1, X, T2), T3, node_3₃(T1, X, U))
if_tappend_3_in_1_gga₆(T1, X, T2, T3, U, tappend_3_out_gga₃(T1, T3, U)) -> tappend_3_out_gga₃(node_3₃(T1, X, T2), T3, node_3₃(U, X, T2))
if_tapplast_3_in_1_gaa₄(L, X, Last, tappend_3_out_gga₃(L, node_3₃(nil_0, X, nil_0), LX)) -> if_tapplast_3_in_2_gaa₅(L, X, Last, LX, tlast_2_in_ag₂(Last, LX))
tlast_2_in_ag₂(X, node_3₃(nil_0, X, nil_0)) -> tlast_2_out_ag₂(X, node_3₃(nil_0, X, nil_0))
tlast_2_in_ag₂(X, node_3₃(L, H, R)) -> if_tlast_2_in_1_ag₅(X, L, H, R, tlast_2_in_ag₂(X, L))
tlast_2_in_ag₂(X, node_3₃(L, H, R)) -> if_tlast_2_in_2_ag₅(X, L, H, R, tlast_2_in_ag₂(X, R))
if_tlast_2_in_2_ag₅(X, L, H, R, tlast_2_out_ag₂(X, R)) -> tlast_2_out_ag₂(X, node_3₃(L, H, R))
if_tlast_2_in_1_ag₅(X, L, H, R, tlast_2_out_ag₂(X, L)) -> tlast_2_out_ag₂(X, node_3₃(L, H, R))
if_tapplast_3_in_2_gaa₅(L, X, Last, LX, tlast_2_out_ag₂(Last, LX)) -> tapplast_3_out_gaa₃(L, X, Last)
if_goal_3_in_2_gaa₅(A, B, C, T, tapplast_3_out_gaa₃(T, B, C)) -> goal_3_out_gaa₃(A, B, C)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

S2T_2_IN_GA₂(s_1₁(X), node_3₃(T, Y, nil_0)) -> S2T_2_IN_GA₂(X, T)
S2T_2_IN_GA₂(s_1₁(X), node_3₃(nil_0, Y, T)) -> S2T_2_IN_GA₂(X, T)
S2T_2_IN_GA₂(s_1₁(X), node_3₃(T, Y, T)) -> S2T_2_IN_GA₂(X, T)

R is empty.
The argument filtering Pi contains the following mapping:
node_3₃(x1, x2, x3) = node_3₂(x1, x3)
nil_0 = nil_0
s_1₁(x1) = s_1₁(x1)
S2T_2_IN_GA₂(x1, x2) = S2T_2_IN_GA₁(x1)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

S2T_2_IN_GA₁(s_1₁(X)) -> S2T_2_IN_GA₁(X)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {S2T_2_IN_GA₁}.
By using the subterm criterion together with the size-change analysis we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

S2T_2_IN_GA₁(s_1₁(X)) -> S2T_2_IN_GA₁(X)
The graph contains the following edges 1 > 1